(0) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#equal(@x, @y) → #eq(@x, @y)
#greater(@x, @y) → #ckgt(#compare(@x, @y))
#less(@x, @y) → #cklt(#compare(@x, @y))
*(@x, @y) → #mult(@x, @y)
+(@x, @y) → #add(@x, @y)
-(@x, @y) → #sub(@x, @y)
add(@b1, @b2) → add'(@b1, @b2, #abs(#0))
add'(@b1, @b2, @r) → add'#1(@b1, @b2, @r)
add'#1(::(@x, @xs), @b2, @r) → add'#2(@b2, @r, @x, @xs)
add'#1(nil, @b2, @r) → nil
add'#2(::(@y, @ys), @r, @x, @xs) → add'#3(sum(@x, @y, @r), @xs, @ys)
add'#2(nil, @r, @x, @xs) → nil
add'#3(tuple#2(@z, @r'), @xs, @ys) → ::(@z, add'(@xs, @ys, @r'))
bitToInt(@b) → bitToInt'(@b, #abs(#pos(#s(#0))))
bitToInt'(@b, @n) → bitToInt'#1(@b, @n)
bitToInt'#1(::(@x, @xs), @n) → +(*(@x, @n), bitToInt'(@xs, *(@n, #pos(#s(#s(#0))))))
bitToInt'#1(nil, @n) → #abs(#0)
compare(@b1, @b2) → compare#1(@b1, @b2)
compare#1(::(@x, @xs), @b2) → compare#2(@b2, @x, @xs)
compare#1(nil, @b2) → #abs(#0)
compare#2(::(@y, @ys), @x, @xs) → compare#3(compare(@xs, @ys), @x, @y)
compare#2(nil, @x, @xs) → #abs(#0)
compare#3(@r, @x, @y) → compare#4(#equal(@r, #0), @r, @x, @y)
compare#4(#false, @r, @x, @y) → @r
compare#4(#true, @r, @x, @y) → compare#5(#less(@x, @y), @x, @y)
compare#5(#false, @x, @y) → compare#6(#greater(@x, @y))
compare#5(#true, @x, @y) → -(#0, #pos(#s(#0)))
compare#6(#false) → #abs(#0)
compare#6(#true) → #abs(#pos(#s(#0)))
diff(@x, @y, @r) → tuple#2(mod(+(+(@x, @y), @r), #pos(#s(#s(#0)))), diff#1(#less(-(-(@x, @y), @r), #0)))
diff#1(#false) → #abs(#0)
diff#1(#true) → #abs(#pos(#s(#0)))
div(@x, @y) → #div(@x, @y)
leq(@b1, @b2) → #less(compare(@b1, @b2), #pos(#s(#0)))
mod(@x, @y) → -(@x, *(@x, div(@x, @y)))
mult(@b1, @b2) → mult#1(@b1, @b2)
mult#1(::(@x, @xs), @b2) → mult#2(::(#abs(#0), mult(@xs, @b2)), @b2, @x)
mult#1(nil, @b2) → nil
mult#2(@zs, @b2, @x) → mult#3(#equal(@x, #pos(#s(#0))), @b2, @zs)
mult#3(#false, @b2, @zs) → @zs
mult#3(#true, @b2, @zs) → add(@b2, @zs)
mult3(@b1, @b2, @b3) → mult(mult(@b1, @b2), @b2)
sub(@b1, @b2) → sub#1(sub'(@b1, @b2, #abs(#0)))
sub#1(tuple#2(@b, @_@1)) → @b
sub'(@b1, @b2, @r) → sub'#1(@b1, @b2, @r)
sub'#1(::(@x, @xs), @b2, @r) → sub'#2(@b2, @r, @x, @xs)
sub'#1(nil, @b2, @r) → tuple#2(nil, @r)
sub'#2(::(@y, @ys), @r, @x, @xs) → sub'#3(diff(@x, @y, @r), @xs, @ys)
sub'#2(nil, @r, @x, @xs) → tuple#2(nil, @r)
sub'#3(tuple#2(@z, @r'), @xs, @ys) → sub'#4(sub'(@xs, @ys, @r'), @z)
sub'#4(tuple#2(@zs, @s), @z) → tuple#2(sub'#5(#equal(@s, #pos(#s(#0))), @z, @zs), @s)
sub'#5(#false, @z, @zs) → ::(@z, @zs)
sub'#5(#true, @z, @zs) → ::(#abs(#0), @zs)
sum(@x, @y, @r) → sum#1(+(+(@x, @y), @r))
sum#1(@s) → sum#2(#equal(@s, #0), @s)
sum#2(#false, @s) → sum#3(#equal(@s, #pos(#s(#0))), @s)
sum#2(#true, @s) → tuple#2(#abs(#0), #abs(#0))
sum#3(#false, @s) → sum#4(#equal(@s, #pos(#s(#s(#0)))))
sum#3(#true, @s) → tuple#2(#abs(#pos(#s(#0))), #abs(#0))
sum#4(#false) → tuple#2(#abs(#pos(#s(#0))), #abs(#pos(#s(#0))))
sum#4(#true) → tuple#2(#abs(#0), #abs(#pos(#s(#0))))
The (relative) TRS S consists of the following rules:
#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)
#div(#0, #0) → #divByZero
#div(#0, #neg(@y)) → #0
#div(#0, #pos(@y)) → #0
#div(#neg(@x), #0) → #divByZero
#div(#neg(@x), #neg(@y)) → #pos(#natdiv(@x, @y))
#div(#neg(@x), #pos(@y)) → #neg(#natdiv(@x, @y))
#div(#pos(@x), #0) → #divByZero
#div(#pos(@x), #neg(@y)) → #neg(#natdiv(@x, @y))
#div(#pos(@x), #pos(@y)) → #pos(#natdiv(@x, @y))
#eq(#0, #0) → #true
#eq(#0, #neg(@y)) → #false
#eq(#0, #pos(@y)) → #false
#eq(#0, #s(@y)) → #false
#eq(#neg(@x), #0) → #false
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)
#eq(#neg(@x), #pos(@y)) → #false
#eq(#pos(@x), #0) → #false
#eq(#pos(@x), #neg(@y)) → #false
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)
#eq(#s(@x), #0) → #false
#eq(#s(@x), #s(@y)) → #eq(@x, @y)
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#eq(::(@x_1, @x_2), nil) → #false
#eq(::(@x_1, @x_2), tuple#2(@y_1, @y_2)) → #false
#eq(nil, ::(@y_1, @y_2)) → #false
#eq(nil, nil) → #true
#eq(nil, tuple#2(@y_1, @y_2)) → #false
#eq(tuple#2(@x_1, @x_2), ::(@y_1, @y_2)) → #false
#eq(tuple#2(@x_1, @x_2), nil) → #false
#eq(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natdiv(#0, #0) → #divByZero
#natdiv(#s(@x), #s(@y)) → #s(#natdiv(#natsub(@x, @y), #s(@y)))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#natsub(@x, #0) → @x
#natsub(#s(@x), #s(@y)) → #natsub(@x, @y)
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#sub(@x, #0) → @x
#sub(@x, #neg(@y)) → #add(@x, #pos(@y))
#sub(@x, #pos(@y)) → #add(@x, #neg(@y))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))
Rewrite Strategy: INNERMOST
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
bitToInt'(::(@x2875451_7, @xs2875452_7), @n) →+ +(*(@x2875451_7, @n), bitToInt'(@xs2875452_7, *(@n, #pos(#s(#s(#0))))))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1].
The pumping substitution is [@xs2875452_7 / ::(@x2875451_7, @xs2875452_7)].
The result substitution is [@n / *(@n, #pos(#s(#s(#0))))].
(2) BOUNDS(n^1, INF)